The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

quicksort(Cons(x, Cons(x', xs))) → part(x, Cons(x, Cons(x', xs)), Cons(x, Nil), Nil)
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
part(x', Cons(x, xs), xs1, xs2) → part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)
part(x, Nil, xs1, xs2) → app(quicksort(xs1), quicksort(xs2))
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs) → quicksort(xs)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
>(S(x), S(y)) → >(x, y)
>(0, y) → False
>(S(x), 0) → True
part[Ite][True][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2)
part[Ite][True][Ite](False, x', Cons(x, xs), xs1, xs2) → part[Ite][True][Ite][False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
part(S(x191021_3), Cons(0, xs), xs1, xs2) →⁺ part(S(x191021_3), xs, Cons(0, xs1), xs2)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(0, xs)].
The result substitution is [xs1 / Cons(0, xs1)].

(2) BOUNDS(n^1, INF)